4.1 KB · ⇊ 3 parts · ⤓ Micron 4.1 KB · ⤓ HTML 45.0 KB

top

Biconditional elimination is the name of two valid rules of inference of propositional logic. It allows for one to infer a conditional from a biconditional. If P ↔ ↔ Q {\displaystyle P\leftrightarrow Q} is true, then one may infer that P → → Q {\displaystyle P\to Q} is true, and also that Q → → P {\displaystyle Q\to P} is true.cite-ref-cohen2007-1-0[1] For example, if it's true that I'm breathing if and only if I'm alive, then it's true that if I'm breathing, I'm alive; likewise, it's true that if I'm alive, I'm breathing. The rules can be stated formally as:

P ↔ ↔ Q ∴ ∴ P → → Q {\displaystyle {\frac {P\leftrightarrow Q}{\therefore P\to Q}}}

and

P ↔ ↔ Q ∴ ∴ Q → → P {\displaystyle {\frac {P\leftrightarrow Q}{\therefore Q\to P}}}

where the rule is that wherever an instance of " P ↔ ↔ Q {\displaystyle P\leftrightarrow Q} " appears on a line of a proof, either " P → → Q {\displaystyle P\to Q} " or " Q → → P {\displaystyle Q\to P} " can be placed on a subsequent line.

• Formal notation

• See also

• References

The biconditional elimination rule may be written in sequent notation:

( P ↔ ↔ Q ) ⊢ ⊢ ( P → → Q ) {\displaystyle (P\leftrightarrow Q)\vdash (P\to Q)}

and

( P ↔ ↔ Q ) ⊢ ⊢ ( Q → → P ) {\displaystyle (P\leftrightarrow Q)\vdash (Q\to P)}

where ⊢ ⊢ {\displaystyle \vdash } is a metalogical symbol meaning that P → → Q {\displaystyle P\to Q} , in the first case, and Q → → P {\displaystyle Q\to P} in the other are syntactic consequences of P ↔ ↔ Q {\displaystyle P\leftrightarrow Q} in some logical system;

or as the statement of a truth-functional tautology or theorem of propositional logic:

( P ↔ ↔ Q ) → → ( P → → Q ) {\displaystyle (P\leftrightarrow Q)\to (P\to Q)}

( P ↔ ↔ Q ) → → ( Q → → P ) {\displaystyle (P\leftrightarrow Q)\to (Q\to P)}

where P {\displaystyle P} , and Q {\displaystyle Q} are propositions expressed in some formal system.

• Logical biconditional

cite-note-cohen2007-11. ↑ citerefcohenCohen, S. Marc. "Chapter 8: The Logic of Conditionals" (PDF). University of Washington. Archived (PDF) from the original on 2022-10-09. Retrieved 8 October 2013.